COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	logic[f81,jmc]		mathematical logic for the practical man
C00003 00003		Most mathematical logicians are not very sympathetic with
C00008 ENDMK
C⊗;
logic[f81,jmc]		mathematical logic for the practical man

Notes:
Need outline

Appendix for the mathematician on why Kreisel should stop fighting
with Russell

outline
1. predicates and functions and the language of first order logic
as a means of expression.  Exercises in formalization

2. First order languages with the interpretation to be determined later.

conditional expressions and first order λs (typed λs)

ekl

first order theories
	integers and natural numbers
	S-expressions and lists
	set theory
	Most mathematical logicians are not very sympathetic with
our objective of using interactive theorem provers to get
computer checked proofs of mathematical theorems, even of
the correctness of computer programs.  It seems to me that this
is partly a result of the history of mathematical logic and
of its evolution away from the early objectives of Russell
and perhaps of Frege.

	Perhaps they supposed, or maybe they are only thought to
have supposed, that mathematics is insecure, because the proofs
are insufficiently rigorous, and that security could be obtained
by building up all proofs from logic using a system like that
of Principia Mathematica.  This plan, if anyone had it, received
several shocks.

	1. The proofs of Principia Mathematica are long for what
they prove and very dull.

	2. The attempts to fput the theory in a final polished form
using type theory left various unpleasant loose ends.

	3. The incompleteness results of Goedel showed that a final
polished form was not to be had.

	4. Goedel's work showed that metamathematics was more
interesting anyway.

	All this leads to a misunderstanding of our present objectives
on the part of mathematical logicians.  Here are some clarifications.

	1. In the first place, we don't suppose that we will have a
final polished system.  Extensions will always be possible.
One may even speculate that the set of mathematically reasonable
axioms is not recursively enumerable, so we'll never have a system
that generates all of them.

	2. The correctness of our system will be no more secure
than that of any other well-checked piece of mathematics.  In fact, for
some time it will be less secure, because it depends on the correctness
of complicated computer programs.  However, it will eventually become
very well checked.  Most important, it confers its own verification
on any proof it has accepted.

	3. We expect that many of the users will not be mathematicians
by training or taste.  Computer programmers will debug proofs as they
debug programs.

	4. The fact that proofs in conventional logical systems are
long and tedious compared to traditional informal proofs iq to be
mitigated by inventing many decision procedures, semi decision
procedures and heuristic proof finders.  We confidently expect that
our fully formal proofs will eventually require less writing
than conventional informal proofs.  Already this is truE for
certain fpagments of the proofs and foR certain proofs of
program correctness in areas where we have done the most work
on the problem.

↓Many years work on this problem will be required before
mathematicq students and mathematicians will findworking with
an interactive prover a cOngenial way of making mathematical
progress and bringing mathematical ideas into a rigorous form.